COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	% The axiomatics of going to the airport
C00005 ENDMK
C⊗;
% The axiomatics of going to the airport

The files on w81,jmc airpor.ax and airpo2.ax, ... contain axiomatizations
of the problem whose solution is walking to the car and driving
to the airport.  The files with extension prf contain proofs.

airpor.ax uses at(x,y,s) exclusively for formulating at relations,
and therefore the fact that the airport is still in county after
I has walked to the car has to be proved.

airpo2.ax if still existing is a start on a version supporting rationality

airpo3.ax doesn't exist

airpo4.ax uses att(x,y) for the non-situation dependent at.  It still
uses walk(z,s) for the situation that results from walking to z in s.

airpo5.ax handles the non situation dependent at better.

airpo6.ax reifies at(x,y) and the actions walk(z) and drive(z).  This
permits want(at(I,airport),S0) and should(I,prog(walk(car),drive(airport)),S0).

	at(I,airport) can be regarded as a semi-intensional expression.  On
the one hand it is a suitable argument to  want  or  know.  On the other
hand, its own arguments are interpreted extensionally.  It can be
regarded as an abbreviation of a fully intensional treatment where
I and airport have standard concepts or standard names.  On the other hand,
this point of view isn't compulsory, and using the semi-intensional
functions directly seems to correspond more closely to the way people
think and therefore presumptively to the way computers should think.

	Here are some random axioms not yet used in proofs:

smart(p) ∧ should(p,a,s) ⊃ occurs(does(p,a),s)

knows(p, should(p,a), s) ⊃ occurs(does(p,a),s)

Can we really get out of having  s within the scope of know?

Is there a significant collection of problems in which

	knows(p,∀x.P(x)) ≡ ∀x.knows(p,P(x))?

If so large simplifications may be possible.